--- layout: fc_discuss_archives title: Message 10 from Frama-C-discuss on May 2017 ---
[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[Frama-c-discuss] Hello and One Dude of EVA (frama-c)



Hello, My name is Francisco Manuel , I'm student of University of Seville.

First, thank for your attention and your time.

I am writing to you, beacause I like modify the code the EVA in frama-c. it
can get us, the depends of a code .c, but I couldn't find to part of code ,
i have modify it.

Basic, I want to connect frama-c with Neo4j( BD Graph ).Now, in java, i
have a code, it read buffer's terminal, and it generate a script. But this,
the code have passed a parser(Transform). for example:

[kernel] Parsing FRAMAC_SHARE/libc/__fc_builtin_for_normalization.i (no
preprocessing)
[kernel] Parsing
../../../Documentos/ocaml/frama-c/Desarrollo/EVA/ejemploC/main.c
(with preprocessing)
[value] Analyzing a complete application starting at main
[value] Computing initial state
[value] Initial state computed
[value] Values of globals at initialization
  y ∈ {0}
  z ∈ {1}
../../../Documentos/ocaml/frama-c/Desarrollo/EVA/ejemploC/main.c:7:[value]
entering loop for the first time
[value] computing for function f <- main.
        Called from ../../../Documentos/ocaml/frama-c/Desarrollo/EVA/
ejemploC/main.c:8.
[value] Recording results for f
[value] Done for function f
[value] computing for function f <- main.
        Called from ../../../Documentos/ocaml/frama-c/Desarrollo/EVA/
ejemploC/main.c:8.
[value] Recording results for f
[value] Done for function f
[value] computing for function f <- main.
        Called from ../../../Documentos/ocaml/frama-c/Desarrollo/EVA/
ejemploC/main.c:8.
[value] Recording results for f
[value] Done for function f
[value] computing for function f <- main.
        Called from ../../../Documentos/ocaml/frama-c/Desarrollo/EVA/
ejemploC/main.c:8.
[value] Recording results for f
[value] Done for function f
[value] computing for function f <- main.
        Called from ../../../Documentos/ocaml/frama-c/Desarrollo/EVA/
ejemploC/main.c:8.
[value] Recording results for f
[value] Done for function f
[value] Recording results for main
[value] done for function main
[value] ====== VALUES COMPUTED ======
[value] Values at end of function f:
  y ∈ {1; 2; 3; 4}
[value] Values at end of function main:
  y ∈ {4}
  z ∈ {1; 2; 3; 4}
[from] Computing for function f
[from] Done for function f
[from] Computing for function main
[from] Done for function main
[from] ====== DEPENDENCIES COMPUTED ======
       These dependencies hold at termination for the executions that
terminate:
[from] Function f:
  y FROM x
  \result FROM x
[from] Function main:
  y FROM \nothing
  z FROM \nothing (and SELF)
[from] ====== END OF DEPENDENCIES ======

↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓parse(Transform)↓↓↓↓↓↓↓↓↓↓↓↓↓↓↓

CREATE (y:Signal {name:'y', Class:'home'})

CREATE (nothing:Depends {name:'nothing', Class:'home'})

CREATE (yisus:Depends {name:'yisus', Class:'home'})

CREATE (z:Signal {name:'z', Class:'home'})

MATCH (SignalD:Depends{name:'nothing'}),(SignalO:Signal{name:'y'})
CREATE (SignalD)-[:In_Dependes]->(SignalO)

MATCH (SignalD:Depends{name:'nothing'}),(SignalO:Signal{name:'z'})
CREATE (SignalD)-[:In_Dependes]->(SignalO)


I'm want to kill to parse. Iḿ studying ocaml of Real World book.I have
thought what I would get ,in the moment EVA generate dependencies and show
in terminal,the information without parse, and i generate scripts.


Could you help me? I'm sorry for my English, and any doubts, You can write
me that I'll be happy to carry the necessary.

Bye and Thanks.

P.D: I don't like graph to make frama-c, I need other thing.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.gforge.inria.fr/pipermail/frama-c-discuss/attachments/20170525/a27b4a37/attachment.html>