Linux Driver Verification » Crude_slicer

I am currently working on verification of Systemsoftware category of SVCOMP tasks. I am using crude_slicer(Build fcd3b927) to slice the tasks.
I am using Ubuntu 16.04 OS. Crude_slicer is using Frama-c Sulfur 2017.
While slicing, ternary expressions are being transformed to "if-else blocks" by using temporary variable. But in some cases the transformation is resulting in gcc compilation errors. So I have tried replicating it with small example. Consider below c-code construct

int m1,m2,b;
    m1=nondet();
    m2=nondet();
    b=((int)((int const) m1 < (int const)m2 ? (int const)m1 : m2));
    if(b==0)
    {
        __VERIFIER_error();
        }

The transformed code construct in slice is,

int m1;
      int m2;
      int b;
      int const tmp;
      m1 = nondet();
      m2 = nondet();
      if (m1 < m2)
               tmp = m1; else
                              tmp = m2;
      b = tmp;
      if (b == 0)
              __VERIFIER_error();

As tmp here in transformed code is declared to be "int const", multiple assignments to it result in GCC compilation error " assignment of read-only variable tmp"

I am using the commands:

cd ./cpa-bam-slicing/lib/native/x86_64-linux/

./frama-c.native -no-autoload-plugins -no-findlib -load-module Crude_slicer.cmxs -machdep gcc_x86_64 -crude_slicer -timeout 400 -no-recognize_wrecked_container_of -widening_threshold 2000 -no-summaries -no-assert_stratification -print -ocode -journal-enable slice.c task.c

I am attaching the input to crude_slicer task.c and sliced code slice.c along with frama_c_journal.ml

Below is the error trace for GCC compilation

The command for GCC compilation:

gcc -c slice.c

test.c: In function ‘main’:
test.c:8:20: error: assignment of read-only variable ‘tmp’
b=((int)((int const) m1 < (int const)m2 ? (int const)m1 : m2));
^
test.c:8:35: error: assignment of read-only variable ‘tmp’
b=((int)((int const) m1 < (int const)m2 ? (int const)m1 : m2));
^