Test to demonstate assert bug on alpine

[thk123]

The user added assert in this test does not get coverage under alpine linux.

I can make this a KNOWNBUG but I thought it would be useful for it to run on CI so everyone can see the problem. The problem seems to be to do with how the assert is handled (possibly caused by musl having a different assert.h when compared to glibc).

GOTO on Ubuntu Linux

main /* main */
        // 0 file regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 7 function main
        signed int x;
        // 1 file regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 7 function main
        x = 0;
        // 2 file regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 8 function main
        ASSERT x == 0 // assertion x==0
        // 3 file regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 8 function main
        IF !(x == 0) THEN GOTO 1
        // 4 file regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 8 function main
        (void)0;
        // 5 no location
     1: SKIP
        // 6 file regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 9 function main
        main#return_value = 0;
        // 7 file regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 9 function main
        dead x;
        // 8 file regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 9 function main
        GOTO 2
        // 9 file regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 10 function main
     2: END_FUNCTION
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

GOTO on Alpine Linux

main /* main */
        // 0 file /cbmc/regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 7 function main
        signed int x;
        // 1 file /cbmc/regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 7 function main
        x = 0;
        // 2 file /cbmc/regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 8 function main
        IF !(x == 0) THEN GOTO 1
        // 3 no location
        TRUE;
        // 4 no location
        GOTO 4
        // 5 file /cbmc/regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 8 function main
     1: ASSERT FALSE // assertion x==0
        // 6 no location
        IF !(0 != 0) THEN GOTO 2
        // 7 no location
        TRUE;
        // 8 no location
        GOTO 3
        // 9 no location
     2: FALSE;
        // 10 no location
     3: SKIP
        // 11 no location
     4: SKIP
        // 12 file /cbmc/regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 9 function main
        main#return_value = 0;
        // 13 file /cbmc/regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 9 function main
        dead x;
        // 14 file /cbmc/regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 9 function main
        GOTO 5
        // 15 file /cbmc/regression/goto-analyzer/sensitivity-test-constants-int/../sensitivity-test-common-files/int_sensitivity_tests.c line 10 function main
     5: END_FUNCTION
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

[thk123]

This is also failing on Windows...

[tautschnig]

Could anyone post the pre-processing result obtained on Alpine Linux?

[thk123]

Sure, one moment. A quick discussion with @martin-cs suggested that replace assert with __CPROVER_assert since this will be transformed uniformly.

[thk123]

Here is the output for doing the following:

test.c

#include <assert.h>

int main()
{
  int x=0;
  assert(x>0);
}

Command on Alpine

$ gcc -E test.c -o test_output.c

test_output.c

# 1 "test_new.c"
# 1 "<built-in>"
# 1 "<command-line>"
# 31 "<command-line>"
# 1 "/usr/include/stdc-predef.h" 1 3 4
# 32 "<command-line>" 2
# 1 "test_new.c"
# 1 "/usr/include/assert.h" 1 3 4
# 1 "/usr/include/features.h" 1 3 4
# 2 "/usr/include/assert.h" 2 3 4
# 19 "/usr/include/assert.h" 3 4

# 19 "/usr/include/assert.h" 3 4
_Noreturn void __assert_fail (const char *, const char *, int, const char *);
# 2 "test_new.c" 2


# 3 "test_new.c"
int main()
{
  int x=0;
  
# 6 "test_new.c" 3 4
 ((void)((
# 6 "test_new.c"
 x>0
# 6 "test_new.c" 3 4
 ) || (__assert_fail(
# 6 "test_new.c"
 "x>0"
# 6 "test_new.c" 3 4
 , "test_new.c", 6, __func__),0)))
# 6 "test_new.c"
            ;
}

Repeating on Ubuntu 16.04 gives:

ubunut_test_output.c

# 1 "test_new.c"
# 1 "<built-in>"
# 1 "<command-line>"
# 1 "/usr/include/stdc-predef.h" 1 3 4
# 1 "<command-line>" 2
# 1 "test_new.c"
# 1 "/usr/include/assert.h" 1 3 4
# 35 "/usr/include/assert.h" 3 4
# 1 "/usr/include/features.h" 1 3 4
# 367 "/usr/include/features.h" 3 4
# 1 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 1 3 4
# 410 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 3 4
# 1 "/usr/include/x86_64-linux-gnu/bits/wordsize.h" 1 3 4
# 411 "/usr/include/x86_64-linux-gnu/sys/cdefs.h" 2 3 4
# 368 "/usr/include/features.h" 2 3 4
# 391 "/usr/include/features.h" 3 4
# 1 "/usr/include/x86_64-linux-gnu/gnu/stubs.h" 1 3 4
# 10 "/usr/include/x86_64-linux-gnu/gnu/stubs.h" 3 4
# 1 "/usr/include/x86_64-linux-gnu/gnu/stubs-64.h" 1 3 4
# 11 "/usr/include/x86_64-linux-gnu/gnu/stubs.h" 2 3 4
# 392 "/usr/include/features.h" 2 3 4
# 36 "/usr/include/assert.h" 2 3 4
# 66 "/usr/include/assert.h" 3 4




# 69 "/usr/include/assert.h" 3 4
extern void __assert_fail (const char *__assertion, const char *__file,
      unsigned int __line, const char *__function)
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));


extern void __assert_perror_fail (int __errnum, const char *__file,
      unsigned int __line, const char *__function)
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));




extern void __assert (const char *__assertion, const char *__file, int __line)
     __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));



# 2 "test_new.c" 2


# 3 "test_new.c"
int main()
{
  int x=0;
  
# 6 "test_new.c" 3 4
 ((
# 6 "test_new.c"
 x>0
# 6 "test_new.c" 3 4
 ) ? (void) (0) : __assert_fail (
# 6 "test_new.c"
 "x>0"
# 6 "test_new.c" 3 4
 , "test_new.c", 6, __PRETTY_FUNCTION__))
# 6 "test_new.c"
            ;
}

[tautschnig]

Would you mind extending your test.c to have some code using the assert macro? I think that is the culprit, rather than the function declarations. Thanks!

[thk123]

@tautschnig D'oh sorry, I've updated the comment with the information.

[tautschnig]

Thanks a lot for the preprocessing, this is very insightful.
See #755 for a related issue where I'd claim the code generated on Ubuntu is strange/has a redundant if. With Alpine Linux the use of || instead of ?: appears to be causing coverage problems.

[tautschnig]

I have cherry-picked this test into #755.

[peterschrammel]

@thk123, I think we can close this one as it will be dealt with as part of #755.

[thk123]

Included in #974