boogie-org/boogieamp

Java parser for the Boogie intermediate verification language

##Boogieamp

This is a Java parser for the Boogie intermediate verification language. Currently, this is work in progress and mostly used for our Joogie and GraVy projects. In the long run, we try to support more and more features of the actual Boogie language. Please look into the unit tests for more details on what is working and what not.

A general description of the Boogie language can be found in this paper. However, this project aims at parsing whatever Boogie can parse currently, so there is a slight difference in the syntax, and boogieamp can parse things that are not described in the paper above.

####Requirements

• Java >= 7
• Junit 4

####Usage
To get an idea how to use the library to parse, process, and create Boogie files look into our Java to Boogie translation or our gradual verifier.

If you plan to use the library in your project, just download the jar file.

####Status We use Travis CI to check the status of Boogieamp:

If the status is red we do not yet pass all unit tests from other Boogie-based projects. However, this does not mean that the libaray is not usable. If you want to see examples of how the library can be used check our other projects.

####Related The following projects are related:

• Ultimate, we stole most of the parser code from an early version of the Ultimate project.
• Smack, a translation from llvm IR into Boogie
• Jar2Bpl, a translation from Java bytecode into Boogie,
• Boogie, a deductive verifier for the Booige language,
• Corral, a whole program analyzer for Boogie,
• Q Program Verifier, a verifier for Booige,
• GraVy, a gradual verifier and infeasible code checker for Boogie.

boogieamp's Issues

Proper computation of dominator relation

in boogie.controlflow.util, we have the loop-head detection and the Hasse diagram construction which could both use a shared dominator relation computation. Right now, they don't share this code, and for both classes, the implementation is super hacky. At some point we should refactor this.

Quantifiers not implemented

boogie.ProgramFactory.mkQuantifierExpression(ILocation, boolean, String[], VarList[], Attribute[], Expression) is not fully implemented!

isFree not yet implemented for CFG

In boogie.controlflow.DefaultControlFlowFactory.constructCfg(ProcedureOrImplementationDeclaration, CfgProcedure)
the is field is not yet used. Frankly, I am not completely sure what is free actually does.