Re: [csmith-dev] Generating ACSL \assigns clauses with programs

[Robert Clausecker <robert.clausecker@fokus.fraunhofer.de>]

Hello Xueyun,

> Take a look of FactMgr::map_stm_effect. I think it has the info you
needed.

I tried to use map_stm_effect to get the desired information, but it
doesn't seem to contain the information I need either. For example, for
a statement

    *param = expression;

where param is parameter to the current function, map_stm_effect
contains the object pointed to by param (as far as I understand). It
seems to not contain information of the form “pointee of param is
modified.”

> Csmith performs path-sensitive inter-procedural analysis. It is realized with the following steps:
> 
> 1) Caller (foo) to callee (bar) handover, where foo passes the knowledge, e.g., y is pointing to x, to bar;
> 2) Effect analysis in bar;
> 3) Callee (bar) to caller (foo) handover, where bar tells foo that x is modified.
> 
> For details, check FunctionInvocationUser::revisit.

I have tried to understand how this mechanism works and I feel like I
haven't understood it well enough to be able to make my own
modifications to the code.

For my application, I believe I need the exact opposite (i.e.
intra-functional path-insensitive analysis) of what the csmith code
does. While it seems like the information I need is available during the
analysis, it seems to be erased (i.e. replaced by contextual
information) by the time meta-data about the function is printed out.

How would you implement tracking context-insensitive data about
functions (i.e. data that is oblivious about where the function is
called)? Where would you add the corresponding code and what modules
have to be modified in order to get the desired result?

Thank you for your help.
Yours sincerely,
Robert Clausecker