How do you statically analyze a single Daml file in a project?

Questions
1

Can you please guide me, how to build .DAR file of the DAML Contract attached below.

image
image1366×768 82.6 KB
. I want to execute this whole example with your static analysis tool. But I am confused how to make dar file of this code? and how you pass this to SMT Solver for verification.

I have taken this example from the daml document link: What is Formal Verification and what it means for Daml

1 Like
2

You can place the source in the skeleton app:

  1. Create a new project with daml new verification
  2. Replace the existing source in daml/Main.daml with the template from the blogpost.
  3. Build the DAR with daml build.

The verification tool is still in experimental state and not released, so to build it you have to check out the Daml repository and build it. Follow the instructions for the necessary steps.
Once you’ve done that, you can run the verification tool (which automatically calls the SMT solver for you) as follows:

bazel run //compiler/daml-lf-verify -- ~/verifcation/.daml/dist/verification-0.0.1.dar -c Main:Account.Account_Transfer -f Main:Account.amount

Adjust the path to your DAR and the template & field name to your own setup.

3 Likes
3

Thanks, I sorted it. I must appreciate your quick and detailed response. It made my learning quick and easy for DAML

1 Like