Сильные указатели на varinfo, которого нет в AST?

Question

Мой плагин Frama-C создает несколько varinfos с makeGlobalVar ~logic:true name type, Эти varinfos не существуют в AST (они являются заполнителями для результатов вызовов для распределения функций в целевой программе, созданных "динамически" во время анализа). Если мой плагин позаботится о том, чтобы не держать сильный указатель на эти varinfos, будет ли у них шанс собрать мусор? Или они зарегистрированы в структуре данных с сильными указателями? Если так, возможно ли сделать эту структуру данных слабой? OCaml не имеет разновидности слабой структуры данных, найденной в литературе для других языков, но нет ничего, что не мог бы исправить периодический явный проход для очистки пустых заглушек.

Теперь, когда я думаю об этом, мне даже не нужно создавать varinfo. Но уже поздно менять мой плагин. То, что я использую в varinfo - это имя и представление типа C. функция makeGlobalVar предлагает гарантию уникальности для имени, что, я думаю, приятно, если оно не создает четкого указателя на него или на его часть в процессе.

Контекст:

Скажем, вы пишете интерпретатор C для выполнения программ на C, которые вызывают malloc() а также free(), Если целевая программа не имеет утечки памяти (она освобождает все, что она выделяет, и никогда не занимает слишком много памяти), вы хотели бы, чтобы интерпретатор вел себя так же.

Answer 1

Если вы явно не зарегистрируете varinfos в одном из Globals таблица, Frama-C не сделает это за вас (и на самом деле, если вы это сделаете, вы должны добавить их объявление в AST и наоборот), так что я думаю, что вы здесь в безопасности. Единственным видимым побочным эффектом в отношении ядра должно быть увеличение Vid счетчик. Однако обратите внимание, что makeGlobalVar сам по себе не гарантирует уникальность vname, но только из vid поле.