--- layout: fc_discuss_archives title: Message 11 from Frama-C-discuss on December 2011 ---
Hello, On 02/12/2011 12:51, Sergio Feo wrote: > VALID or NOT VALID. However, they are not visible when running Frama-C > from the command line with 'frama-c -rte -val rte_test.c'. > > The program analyzed is a minimal example with a division where rte > generates the assertion that the divisor is not 0. The result of issuing > that command is the output of the value analysis plug-in but no mention > of the generated assertions is made. The use of the 'report' plug-in > also yields no results ("No status to report" is displayed). > The issue is that the order in which rte, val and report will be launched is not specified, as these are three independent analyses operating at the same stage (see Frama-C's developer manual section 5.13 for more info about the various stages of a Frama-C run). It is possible to instruct Frama-C to perform the analyses in a specified order with the -then option: frama-c -rte rte_test.c -then -val -then -report should do what you want. Note that rte_test.c must be placed before the first -then (otherwise, your initial project would not have any source file. See user manual section 3.3.1 for more information about -then and its project-aware sibling -then-on) Best regards, -- E tutto per oggi, a la prossima volta Virgile