--- layout: fc_discuss_archives title: Message 71 from Frama-C-discuss on February 2011 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

No subject



- 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