Some boogie programs do not parse
Opened this issue · 0 comments
I found 3 programs in this repository that do not parse
First
ldv-consumption/32_7a_cilled_true-unreach-call_linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main2_sequence_infinite_withcheck_stateful.cil.out.c_.bpl
does not parse due to use of a reserved type name (real
) as a variable name
procedure dm_tm_create_non_blocking_clone(real: int)
Second
ldv-consumption/linux-3.8-rc1-32_7a-drivers--md--persistent-data--dm-persistent-data.ko-ldv_main3_true-unreach-call.cil.out.c_.bpl
does not parse for the same reason as the above boogie program
Third
ldv-linux-3.16-rc1/43_2a_consumption_linux-3.16-rc1.tar.xz-43_2a-drivers--gpu--drm--via--via.ko-entry_point_true-unreach-call.cil.out.c_.bpl
does not parse due to the use of a reserved keyword (then
, used in if-then-else expressions) as a variable name.
procedure time_diff(now: int, then: int)
I suspect this was a bug in SMACK
when these boogie programs were created but I do not have a working copy of SMACK to test if this is still a bug.