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]

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

  • Subject: [Frama-c-discuss] Hello and One Dude of EVA (frama-c)
  • From: fraromrom at gmail.com (francisco manuel romero romero)
  • Date: Thu, 25 May 2017 18:29:58 +0200
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>