2021-02-27 11:40 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0001126Frama-CKernelpublic2014-02-12 16:59
Reporterpherrmann 
Assigned Tovirgile 
PrioritynormalSeverityminorReproducibilityalways
StatusclosedResolutionfixed 
Product VersionFrama-C GIT, precise the release id 
Target VersionFixed in VersionFrama-C Oxygen-20120901 
Summary0001126: AST check failure : problem with generated block-local variables
DescriptionOn submitted file :

frama-c -check failchek.c

produces

failcheck.c:40:[kernel] failure: [AST Integrity Check] initial AST
                  In function _gnutls_epoch_set_cipher_suite, variable tmp_0 is supposed to be local to a block but not mentioned in function's locals.
[kernel] error occurring when exiting Frama-C: stopping exit procedure.


Also, use of

frama-c failcheck -print -then -check

does not produce the problem, while

frama-c failcheck.c -then -check

does, thus -print seems to have an unintended side-effect.
TagsNo tags attached.
Attached Files
  • c file icon failcheck.c (1,447 bytes) 2012-03-20 11:08 -
    
    typedef struct gnutls_session_t {
      int f;
    } gnutls_session_t;
    
    typedef void(*gnutls_cipher_algorithm_t)(int);
    
    typedef void(*gnutls_mac_algorithm_t)(int);
    
    #define GNUTLS_CIPHER_UNKNOWN 0
    #define GNUTLS_MAC_UNKNOWN 0
    #define GNUTLS_E_INTERNAL_ERROR 0
    #define GNUTLS_E_UNWANTED_ALGORITHM 0
    
    typedef struct record_parameters_st {
      int initialized;
      gnutls_cipher_algorithm_t cipher_algorithm;
      gnutls_mac_algorithm_t mac_algorithm;
    } record_parameters_st;
    
    typedef struct cipher_suite_st {
      int a;
    } cipher_suite_st;
    
    int
    _gnutls_epoch_set_cipher_suite (gnutls_session_t session,
                                    int epoch_rel, cipher_suite_st * suite)
    {
      gnutls_cipher_algorithm_t cipher_algo;
      gnutls_mac_algorithm_t mac_algo;
      record_parameters_st *params;
      int ret;
    
      ret = _gnutls_epoch_get (session, epoch_rel, &params);
      if (ret < 0)
        return gnutls_assert_val (ret);
    
      if (params->initialized
          || params->cipher_algorithm != GNUTLS_CIPHER_UNKNOWN
          || params->mac_algorithm != GNUTLS_MAC_UNKNOWN)
        return gnutls_assert_val (GNUTLS_E_INTERNAL_ERROR);
    
      cipher_algo = _gnutls_cipher_suite_get_cipher_algo (suite);
      mac_algo = _gnutls_cipher_suite_get_mac_algo (suite);
    
      if (_gnutls_cipher_is_ok (cipher_algo) != 0
          || _gnutls_mac_is_ok (mac_algo) != 0)
        return gnutls_assert_val (GNUTLS_E_UNWANTED_ALGORITHM);
    
      params->cipher_algorithm = cipher_algo;
      params->mac_algorithm = mac_algo;
    
      return 0;
    }
    
    c file icon failcheck.c (1,447 bytes) 2012-03-20 11:08 +

-Relationships
+Relationships

-Notes

~0004708

Fix committed to stable/neon branch.
+Notes

-Issue History
Date Modified Username Field Change
2012-03-20 11:08 pherrmann New Issue
2012-03-20 11:08 pherrmann File Added: failcheck.c
2012-03-20 21:05 yakobowski Status new => assigned
2012-03-20 21:05 yakobowski Assigned To => virgile
2012-03-30 16:44 svn
2012-03-30 16:44 svn Status assigned => resolved
2012-03-30 16:44 svn Resolution open => fixed
2012-09-19 17:15 signoles Fixed in Version => Frama-C Oxygen-20120901
2012-09-19 17:16 signoles Status resolved => closed
2013-12-19 01:12 Source_changeset_attached => framac master b9c82670
2014-02-12 16:54 Source_changeset_attached => framac stable/neon b9c82670
2014-02-12 16:59 Note Added: 0004708
2014-02-12 16:59 Status closed => resolved
+Issue History