search

runtimeverification / michelson-semantics

A K semantics of Tezos' Michelson language.
Other
17 stars 6 forks source link

michelson: add file inclusion functionality #179

Closed sskeirik closed 3 years ago

sskeirik commented 3 years ago

Currently, relative paths are interpreted relative to ./kmich and not to the file which we are importing from.

This is not ideal, but I'm not sure of the best way to fix this.

My thought is we can merge this now and come back and fix this issue later. Thoughts?

Fixes: runtimeverification/firefly-michelson#16

ehildenb commented 3 years ago

Hmmmm, that's unfortunate. Maybe for the michelson.md we can pass in (as configuration variables) (i) the current directory, and (ii) the path to the input file that is being used?

sskeirik commented 3 years ago

@nishantjr I am trying to add an additional input to the program (the definition directory) and it works for the llvm interpreter but the symbolic driver isn't working right. Could you take a look at this or could we discuss this tomorrow at the standup? Thanks.

sskeirik commented 3 years ago

@ehildenb This is ready for review. I updated the file inclusion functionality so that:

  1. it only applies to the LLVM backend
  2. it is always relative to the input test file