Commits

Nadia Polikarpova committed cbda772 Draft

Running instructions use SumMax example now.

  • Participants
  • Parent commits 937bebe

Comments (0)

Files changed (1)

 
 =Running Boogaloo=
 
+We are using <<file examples/SumMax.bpl>> as an example in this section.
+
 You can run Boogaloo in one of the three modes.
 
 ===Execution===
 
 {{{
-boogaloo MyProgram.bpl
+boogaloo SumMax.bpl
 }}}
 
-This will execute procedure {{{Main}}} in MyProgram.bpl and display the values of global variables when it terminates.
+This will execute procedure {{{Main}}} in SumMax.bpl and display the values of global variables when it terminates.
 You can specify an alternative entry point through the {{{--entry}}} flag.
 The entry point cannot have any in- or out-parameters.
 
 ===Exhaustive testing===
 
 {{{
-boogaloo test --proc MyProcedure MyProgram.bpl
+boogaloo test --proc SumMax SumMax.bpl
 }}}
 
-This will execute procedure {{{MyProcedure}}} in MyProgram.bpl on all inputs within a default range
+This will execute procedure {{{SumMax}}} in SumMax.bpl on all inputs within a default range
 and display a summary of the test cases.
 Input values are generated for all in-parameters and global variables that are [[http://en.wikipedia.org/wiki/Live_variable_analysis|live]] in the procedure body.
 You can change the input range through the {{{--limits}}} flag.
 ===Random testing===
 
 {{{
-boogaloo rtest --proc MyProcedure MyProgram.bpl
+boogaloo rtest --proc SumMax SumMax.bpl
 }}}
 
-This will execute procedure {{{MyProcedure}}} in MyProgram.bpl on random inputs
+This will execute procedure {{{SumMax}}} in SumMax.bpl on random inputs
 and display a summary of the test cases.
 Use the {{{-n}}} flag to control the number of test cases to be generated.
 Check {{{boogaloo --help}}} for additional options.