@@ -15,14 +15,14 @@ parse_property_file()
1515{
1616 local fn = $1
1717
18- cat $fn | sed 's/[[:space:]]//g' | perl -n -e '
19- if(/^CHECK\(init\((\S+)\(\)\),LTL\((\S+)\)\)$/) {
20- print "ENTRY=$1\n";
21- print "PROP=\"label\"\nLABEL=\"$1\"\n" if($2 =~ /^G!label\((\S+)\)$/);
18+ cat $fn | sed 's/[[:space:]]//g' | perl -n -e '
19+ if(/^CHECK\(init\((\S+)\(\)\),LTL\((\S+)\)\)$/) {
20+ print "ENTRY=$1\n";
21+ print "PROP=\"label\"\nLABEL=\"$1\"\n" if($2 =~ /^G!label\((\S+)\)$/);
2222 print "PROP=\"unreach_call\"\n" if($2 =~ /^G!call\(__VERIFIER_error\(\)\)$/);
23- print "PROP=\"memsafety\"\n" if($2 =~ /^Gvalid-(free|deref|memtrack)$/);
24- print "PROP=\"overflow\"\n" if($2 =~ /^G!overflow$/);
25- print "PROP=\"termination\"\n" if($2 =~ /^Fend$/);
23+ print "PROP=\"memsafety\"\n" if($2 =~ /^Gvalid-(free|deref|memtrack)$/);
24+ print "PROP=\"overflow\"\n" if($2 =~ /^G!overflow$/);
25+ print "PROP=\"termination\"\n" if($2 =~ /^Fend$/);
2626}'
2727}
2828
@@ -58,12 +58,12 @@ process_graphml()
5858 else
5959 TYPE = "violation_witness"
6060 fi
61- cat $LOG . witness | perl -p -e "s/(<graph edgedefault=\" directed\" >)/\$1\\E
62- <data key=\" witness-type\" >$(echo $TYPE)<\/data>
63- <data key=\" producer\" >$(echo $TOOL_NAME)<\/data>
64- <data key=\" specification\" >$(<$PROP_FILE)<\/data>
65- <data key=\" programfile\" >$(echo $BM | sed 's8/8\\/8g')<\/data>
66- <data key=\" programhash\" >$(sha1sum $BM | awk '{print $1}')<\/data>
61+ cat $LOG . witness | perl -p -e "s/(<graph edgedefault=\" directed\" >)/\$1\\E
62+ <data key=\" witness-type\" >$(echo $TYPE)<\/data>
63+ <data key=\" producer\" >$(echo $TOOL_NAME)<\/data>
64+ <data key=\" specification\" >$(<$PROP_FILE)<\/data>
65+ <data key=\" programfile\" >$(echo $BM | sed 's8/8\\/8g')<\/data>
66+ <data key=\" programhash\" >$(sha1sum $BM | awk '{print $1}')<\/data>
6767 <data key=\" architecture\" >${BIT_WIDTH##--} bit<\/data>\\Q/"
6868 fi
6969}
0 commit comments