/*未定义序列*/来自 Frama-C 的切片代码

Question

我正在尝试使用 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;
}

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

Answer 1

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

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

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

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