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]

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