--- layout: fc_discuss_archives title: Message 72 from Frama-C-discuss on October 2013 ---
Hello, 2013/10/17 Nanci Naomi <nnarai at gmail.com>: >> 3. Buy/rent a faster machine. > > > our machine is a Mac Boo Pro, processor: 2.9 GHz Intel Core i7, memory: 8 > GB. > this example with about 2,000 VCs is verified in about 10 minutes, but our > original source code with 6,000 VCs is analyzed very slowly, the Alt-ergo > prover takes about 24 hours without finishing the analysis. Probably the main issue is that each time you make a modification, you need to redo *all* the VCs. Not very usable in practice. GNATprove (technology similar to Frama-C but applied on Ada) provides a cache mechanism that avoids re-doing VCs that haven't changed. Maybe a future improvement for Frama-C? > then, we replaced the suggested annotation by this one: > /*@ assigns flag; > @ ensures (a && !a1) ==> flag == time1; > @ ensures !(a && !a1) ==> \old(flag); > @*/ > if(a == TRUE && a1 == FALSE) > { > flag = time1; > } > > it ran, but how do this work? > Sorry, but I did not understand how these annotations will make possible to > run the analysis in a shorter time. [Claude will probably correct me. ;-) ] This annotation substitutes, within the logical framework of Jessie, the "if" piece of code by the given assertion which is equal to one (or two?) logical formula (((a && !a1) ==> flag == time1) && ( !(a && !a1) ==> \old(flag))). Then, when the weakest precondition generation algorithm is applied, this unique logical formula is used instead of the 3 logical formulas generated from the "if" construct, thus the reduction on the number of VCs. You would obtain the same result by putting part of your code into another function, with a proper contract to represent the corresponding code and call it from the original function. Which brings me to a fourth proposal: 4. Cut the original code into several sub functions, with for each called function a contract summarizing the corresponding code. I know this approach is sometimes used into other formalisms, for example using LOCAL_OPERATIONS in B Method. Best regards, david