Skip to content

Commit c50fb3a

Browse files
author
Aalok Thakkar
committed
Added assigns clauses for loops
1. Renamed cprover_contract_assigns_opt to cprover_contract_assigns as it did not have unit production. 2. Created cprover_contract_assigns_opt that supports unit productions 3. Added cprover_contract_assigns_opt to iteration_statement. 4. Renamed loop_invariant_opt to cprover_contract_invariant_opt for consistency. 5. Renamed loop_decreases_opt to cprover_contract_decreases_opt for consistency. This adds support for parsing assigns clauses for loops.
1 parent 9136a73 commit c50fb3a

File tree

0 file changed

+0
-0
lines changed

    0 file changed

    +0
    -0
    lines changed

    0 commit comments

    Comments
     (0)