1

我正在尝试使用 Frama-C 对代码进行切片。

源代码是

static uint8_T ALARM_checkOverInfusionFlowRate(void)
{
uint8_T ov;
ov = 0U;
if (ALARM_Functional_B.In_Therapy) {
  if (ALARM_Functional_B.Flow_Rate > ALARM_Functional_B.Flow_Rate_High) {
     ov = 1U;
   } else if (ALARM_Functional_B.Flow_Rate >
       ALARM_Functional_B.Commanded_Flow_Rate * div_s32
           (ALARM_Functional_B.Tolerance_Max, 100) +
                  ALARM_Functional_B.Commanded_Flow_Rate) {
                     ov = 1U;
                  } else {
                      if (ALARM_Functional_B.Flow_Rate > ALARM_Functional_B.Commanded_Flow_Rate *                div_s32(ALARM_Functional_B.Tolerance_Min, 100) + ALARM_Functional_B.Commanded_Flow_Rate) {
                         ov = 2U;
                      }
                }
      }
  return ov;
}

当我使用 Frama-C 对代码进行切片时，我得到以下信息。我不知道这个“未定义的序列”是什么意思。

static uint8_T ALARM_checkOverInfusionFlowRate(void)
{
  uint8_T ov;
  ov = 0U;
  if (ALARM_Functional_B.In_Therapy)
    if ((int)ALARM_Functional_B.Flow_Rate > (int)ALARM_Functional_B.Flow_Rate_High)
      ov = 1U;
    else {
      int32_T tmp_0;
      {
        /*undefined sequence*/
        tmp_0 = div_s32((int)ALARM_Functional_B.Tolerance_Max,100);
      }
      if ((int)ALARM_Functional_B.Flow_Rate > (int)ALARM_Functional_B.Commanded_Flow_Rate * tmp_0 + (int)ALARM_Functional_B.Commanded_Flow_Rate)
        ov = 1U;
      else {
        int32_T tmp;
        {
          /*undefined sequence*/
          tmp = div_s32((int)ALARM_Functional_B.Tolerance_Min,100);
        }
        if ((int)ALARM_Functional_B.Flow_Rate > (int)ALARM_Functional_B.Commanded_Flow_Rate * tmp + (int)ALARM_Functional_B.Commanded_Flow_Rate)
          ov = 2U;
      }
    }
  return ov;
}

感谢任何帮助解释为什么会发生这种情况。

4

1 回答 1

3

/* undefined sequence */in a block 仅仅意味着该块是在解析时的代码规范化期间生成的，但就 C 语义而言，组成它的语句之间没有序列点。例如x++ + x++将被归一化为

 {
    /*undefined sequence*/
    tmp = x;
    x ++;
    tmp_0 = x;
    x ++;
    ;
 }

在内部，这样一个序列中的每个语句都装饰有可访问以进行写入或读取的位置列表（使用-kernel-debug 1with-print在输出中查看它们）。与选项-unspecified-access一起使用-val将检查此类访问是否正确，即序列内最多有一个语句写入给定位置，如果是这种情况，则没有对其的读取访问（除了构建值它被分配给）。此外，此选项不处理序列内函数调用中发生的副作用。有一个特殊的插件，但它还没有发布。

最后请注意，自从 Frama-C Neon 以来，评论只显示/*sequence*/，这对用户来说似乎不那么令人生畏。实际上，原始代码可能是正确的，也可能显示出未定义的行为，但句法分析太弱，无法在一般情况下做出决定。例如，只要(*p)++ + (*q)++不重叠都是正确的。这就是为什么规范化阶段只指出序列并将其留给更强大的分析插件来检查是否可能存在问题。pq

于 2014-08-19T17:07:42.280 回答