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] frama-c slice how to choose entry to get pragma ctrl

  • Subject: [Frama-c-discuss] frama-c slice how to choose entry to get pragma ctrl
  • From: tdjackey at (tdjackey)
  • Date: Thu, 30 Jun 2016 03:00:51 +0800
  • References: <>

Hi, I got some problem  about to get a CTRL slice;
I try to analysis OPENSSL <>

so I use
frama-c ./ssl/d1_both.c  -main dtls1_process_heartbeat -slicing-value memcpy -cpp-command "gcc -C -E -I ./include/ -I ./" -then-on 'Slicing export' -print 
It gets nothing ; 
I changed into this 

frama-c ./ssl/d1_both.c  -main dtls1_process_heartbeat -slicing-level 3 -slice-pragma memcpy -cpp-command "gcc -C -E -I ./include/ -I ./" -then-on 'Slicing export' -print 
and I got a crash ; 
    Called from file "src/kernel/", line 732, characters 2-9
         Called from file "src/kernel/", line 212, characters 4-8
         Unexpected error (Kernel_function.No_Definition).
         Please report as 'crash' at <>.
         Your Frama-C version is Fluorine-20130601.
         Note that a version and a backtrace alone often do not contain enough

My Question is how can I get a slice like that ? 

function A (){



function B (){


function C (){




what I want is everything todo with memcpy()  So I want to keep A C and delete B 
So how should I choose an entry point ? or How to choose the pragma ??
Hope I’d make my question clear and I have been confused for days 
Thanks a lot !!!!!!!
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <>