Frama-C-discuss mailing list archives
This page gathers the archives of the old Frama-C-discuss archives, that was hosted by Inria's gforge before its demise at the end of 2020. To search for mails newer than September 2020, please visit the page of the new mailing list on Renater.
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
- Subject: No subject
- From: firstname.lastname@example.org ()
- Date: Thu, 24 Feb 2011 12:45:28 -0000
- the memory locations read or written in the assembly code are not counted= ; - the assembly code is ignored by the value analysis, which may make the results used by input/output computations incorrect by changing aliasing or making code that appears unreachable reachable. If you want to improve this yourself for a particular compiler, the lines to change are | Asm _ -> warning_once_current "assuming assembly code has no effects in function %t" pretty_current_cfunction_name; Dataflow.Default in value/eval.ml and corresponding cases in the Inout plug-in. If this is the last limitation preventing industrial applications that would save heaps of cash, you may also reach one of the two contacts listed on http://frama-c.com/contact.html to discuss whether it can be done and supported by the original developers. Do not worry that the subject will feel un-researchy: they have sold much worse. Pascal _______________________________________________ Frama-c-discuss mailing list Frama-c-discuss at lists.gforge.inria.fr http://lists.gforge.inria.fr/cgi-bin/mailman/listinfo/frama-c-discuss