--- layout: fc_discuss_archives title: Message 71 from Frama-C-discuss on February 2011 ---
- 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