search

m-carrasco / TinyBCT

MIT License
3 stars 2 forks source link

Create boggie expressions programatically instead of using raw string manipulation #7

Open rcastano opened 6 years ago

rcastano commented 6 years ago

So far we've been directly generating strings to prototype and iterate quickly. At this point it'd help us to modularize the code and use the Boogie API.

rcastano commented 6 years ago

@m7nu3l feel free to break this down, AFAIK you're working on modularizing the code first, without using the Boogie API.

m-carrasco commented 6 years ago

Boogie code is generated in the BoogieGenerator class, as you said this is not using the Boogie API. It encapsulates and modularizes the raw string generation for boogie expressions and statements.

Almost every string manipulation in InstructionTranslator.cs were removed, only a few cases remain alive.

You may find raw string manipulation outside of BoogieGenerator in the following methods: