Menu

#40 Parens not matching up in VC goals

open-accepted
Verifier (14)
5
2012-07-20
2012-07-20
Chuck Cook
No

In some cases the parenthesis don't match up in the goals for the VC. This happens in both the web interface and when outputting to .asrt files. Here is an example:

VC: 0_2:
Requires Clause of Push in Procedure Do_Nothing: Do_Nothing_Realiz.rb(8)

Goal:
(|S'| + 1) <= Max_Depth)

Given:
1: (Last_Char_Num > 0)
2: (min_int <= 0)
3: (0 < max_int)
4: (1 <= Max_Depth)
5: (min_int <= Max_Depth) and (Max_Depth <= max_int)
6: (|S| <= Max_Depth)
7: (|S| > 0)
8: S = (<Next_Entry'> o S')

Notice the right paren after Max_Depth with no matching left paren. I ran this test on Do_Nothing_Realiz.rb with the flags -vcs and -listvcs. It happens on both realizations and facilities.

Discussion

  • Yu-Shan Sun

    Yu-Shan Sun - 2012-07-20
    • status: open --> open-accepted
     
  • Yu-Shan Sun

    Yu-Shan Sun - 2012-07-20

    Works on my branch of the compiler using the Netbeans WebUI setup... It could be that I changed something on my end to make that work. Will test my jar using the Old-Resolve machine to be sure.

     

Log in to post a comment.